T:Type, R:(TT).
Trans(T;x,y.R(x,y))
 (L:(T List).
 (i:{0..(||L|| - 1)}. R(L[i],L[(i+1)]))
  (((null(L)))  R(last(L),hd(L)))
  (aL. bL. R(a,b))) 

latex

Definitions	x:A. B(x), , P  Q, x(s1,s2), A, t  T, Top, S  T, A  B, False, x,y. t(x;y), b, null(as), xL. P(x), tt, ff, if b then t else f fi , True, SQType(T), {T}, i  j , {i..j}, i  j < k, P & Q, T, last(L), hd(l), l[i], Y, nth_tl(n;as), i z j, b, i <z j, ||as||, P  Q, Dec(P), P  Q, , Trans(T;x,y.E(x;y)), (x  l), x:A. B(x), A c B
Lemmas	not wf, assert wf, null wf3, top wf, last wf, hd wf, int seg wf, length wf1, select wf, trans wf, l member wf, false wf, true wf, nil member, nat wf, decidable int equal, nat properties, ge wf, le wf, decidable lt, squash wf, non neg length